Math 512: Finite Model Theory k-variable logic

John Baldwin

March 4, 1997

references - Vaananen, chapter 4, E and F chapter 2, Poizat (JSL)

Complexity of a formula: length, quantifier rank, quantifier complexity (number of alternations), number of variables

Define L_{ω_{1},ω}, L_{∞,ω}

0.1 Definition. FO^{k} denotes first order logic with only k-variables free or bound; L^{k} = L_{ω_{1},ω}^{k} similarly. L^{ω} = ⋃_{k} L^{k}.

0.2 Example. Let τ contain only <. There are FO^{2} formulas ψ_{n}(x_{1}) and χ_{n} such that for any linearly ordered structure A, A ⊧ ψ_{n}(a) iff a is the nth element in the order and A ⊧ χ_{n} iff A = n.

Let ψ_{0}(x_{1}) be (∀x_{2})x_{2} ≮ x_{1}. Let ψ_{n+1}(x_{1}) be

(∀x_{2})[x_{2} < x_{1} ↔ ⋁_{i≤n}(∃x_{1})(x_{1} = x_{2} ∧ ψ_{i}(x_{1})).

Let χ_{n} be (∃x_{1})ψ_{n−1}(x_{1}) ∧ ¬(∃x_{1})ψ_{n}(x_{1}).

Vaananen has different formulas which are only in F O^{3}.

Theorem 0.3 (Barwise). FP is contained in L^{ω}.

Proof. More precisely if S is k-ary and there are ℓ variables in ϕ, [LF P_{\overline{u},X}ϕ]\overline{x} can be expressed by ψ(\overline{x}) with ψ ∈ L^{k+ℓ}.

[LF P_{\overline{u},X}ϕ]\overline{x} ≡ ψ(\overline{x}) =: ⋁_{i<ω} ψ_{i}(\overline{x}),

where

ψ_{0}(\overline{x}) =: ¬x_{1} = x_{1}
ψ_{i+1}(\overline{x}) =:

the result of replacing each occurence of X\overline{t} (for any term \overline{t}) in ϕ(\overline{x}, X) by

(∃\overline{y})(\overline{y} = \overline{t} ∧ (∃\overline{x})(\overline{x} = \overline{y} ∧ ψ_{i}(\overline{x}))).

(Note that some of the variables of \overline{x} may occur in \overline{t}. We must switch quantifiers twice as \overline{y} might become bound in ψ_{i}.)

0.4 Lemma. Let L be a finite relational language. Every class of finite L-structures is definable in L_{ω_{1},ω}. Form L^{+} by adding < to L. Every class K of finite linearly ordered L^{+}-structures is definable in L^{ω}.

Proof. For the first take the disjunction of the (existential quantifications) of the diagrams of members of K. For the first use, the fact ( 0.2) that every ordered structure is definable using 3 quantifiers and use m more to code any m-ary relation.

This leaves the L^{k} as interesting languages even with order. Recall:

0.5 Definition. There exists an m-back and forth between A and B if there is a sequence, ⟨I_{j}; j ≤ m⟩, such that

1. Every I_{j} is a nonempty set of partial isomorphisms between A and B.

2. (forth) If p ∈ I_{j+1} and a ∈ A − dom p, there is a q ∈ I_{j} with a ∈ dom q and q ⊇ p.

3. (back) If p ∈ I_{j+1} and b ∈ B − rng p, there is a q ∈ I_{j} with b ∈ rng q and q ⊇ p.

Two structures A, B are equivalent for sentences of quantifier depth m if and only if there exists an m- back and forth. (E and F say m-isomorphic). A and B are elementarily equivalent just if there is an m-back and forth for every m < ω.

0.6 Definition. A and B are partially isomorphic if there is an I such that

1. I is a nonempty set of partial isomorphisms between A and B.

2. (forth) If p ∈ I and a ∈ A − dom p, there is a q ∈ I with a ∈ dom q and q ⊇ p.

3. (back) If p ∈ I and b ∈ B − rng p, there is a q ∈ I with b ∈ rng q and q ⊇ p.

0.7 Lemma. A and B are partially isomorphic if and only if they satisfy the same sentences in L_{∞,ω}.

Note two countable partially isomorphic structures are isomorphic.

An s partial isomorphism between A and B is a sequence p of at most s elements of A × B which form the graph of a partial isomorphism. Given such a p, For i < lg(p), p(a, b/i) is the result of replacing the ith-pair by ⟨a, b⟩ if i < lg(p).

The pebble game is described on page 48 of E and F. We give the partial isomorphism version.

0.8 Definition. There exists an s-m-back and forth between A and B if there is a sequence, ⟨I_{j}; j ≤ m⟩, such that

1. Every I_{j} is a nonempty set of s-partial isomorphisms between A and B.

2. (forth) If p ∈ I_{j+1} and a ∈ A − dom p,

(a) if lg(p) < s, there is a b ∈ B − rng p such that p ∪ {⟨a, b⟩} ∈ I_{j};

(b) if lg(p) = s, there is a b ∈ B − rng p such that for each i < s, there is a b ∈ B − rng p such that p(a, b/i) ∈ I_{j}.

3. (back) If p ∈ I_{j+1} and b ∈ B − rng p,

(a) if lg(p) < s, there is an a ∈ A − dom p such that p ∪ {⟨a, b⟩} ∈ I_{j};

(b) if lg(p) = s, for each i < lg(p), there is an a ∈ A − dom p such that p(a, b/i) ∈ I_{j}.

0.9 Definition. W_{m}^{s}(A, B) be the set of s-partial isomorphisms p from A to B such that duplicator has a winning strategy for the game G_{m}^{s}(A, dom p, B rng p).

Here is a canonical form for describing elements in F O^{s}. For \overline{a} ∈ A^{<s}, we define for each m a formula ψ_{a_{0},...a_{k−1}}^{m}(v_{0}, … v_{k−1}), k < s.

Fix lg(\overline{a}) = k ≤ s, k′ = min(k + 1, s). Let \overline{a}^{i} denote the result of omitting the ith term from \overline{a} if i < k and \overline{a}^{i} = \overline{a} if i ≥ k.

ψ0 ; \overline{a} = ⋀ quantifier free diagram of\overline{a}

ψm+1 ; \overline{a}(\overline{v}) = ψ0 ; \overline{a}(\overline{v}) ∧ ⋀_{i<k′} ⋀_{\overline{a}^{i}⊆\overline{b}∈A^{k′}}(∃v_{i})ψm ; \overline{b}(\overline{v}^{i}v_{i}) ∧ (∀v_{i}) ⋁_{\overline{a}^{i}⊆\overline{b}∈A^{k′}} ψm ; \overline{b}(\overline{v}^{i}v_{i}).

0.10 Proposition. Let dom p = \overline{a}, rng p = \overline{b}. The following are equivalent:

1. There is an s-m-back and forth between A and B with p ∈ I_{m}

2. (A, \overline{a}) and (B, \overline{b}) satisfy the same s-variable sentences with quantifier depth at most m.

3. B ⊧ ψm ; \overline{a}(\overline{b}).

4. Duplicator has a winning stategy for G_{m}^{s}(A, dom p, B rng p).

Now the infinitary version.

0.11 Definition. A and B are s-partially isomorphic if there is an I such that 1. I is a nonempty set of s-partial isomorphisms between A and B.

2. (forth) If p ∈ I and a ∈ A − dom p,

(a) if lg(p) < s, there is a b ∈ B − rng p such that p ∪ {⟨a, b⟩} ∈ I;

(b) if lg(p) = s, there is a b ∈ B − rng p such that for each i < s, there is a b ∈ B − rng p such that p(a, b/i) ∈ I.

3. (back) If p ∈ I and b ∈ B − rng p,

(a) if lg(p) < s, there is an a ∈ A − dom p such that p ∪ {⟨a, b⟩} ∈ I;

(b) if lg(p) = s, for each i < lg(p), there is an a ∈ A − dom p such that p(a, b/i) ∈.

0.12 Proposition. The following are equivalent:

1. A and B are s-partially isomorphic.

2. A ≡_{L^{s}} B.

3. Duplicator has a winning stategy for the infinite s-pebble game on A, B.

The previous two results hold for structures of all cardinalities and just report various aspects of the same notion. The following result holds only for finite models.

0.13 Theorem. Suppose A and B are finite. The following are equivalent:

1. A ≡_{F O^{s}} B.

2. A ≡_{L^{s}} B.

3. Duplicator has a winning stategy for the infinite s-pebble game on A, B.

Proof. A ≡_{F O^{s}} B implies that for all m, W_{m}^{s}(A, B) ≠ ∅. Note that W_{m−1}^{s}(A, B) ⊇ W_{m}^{s}(A, B). But there are only finitely many possibilities so some W_{m−1}^{s}(A, B) = W_{m}^{s}(A, B). But then W_{m}^{s}(A, B) is an s-partial isomorphism between A and B so A ≡_{L^{s}} B.

While L^{k} and F O^{k}-equivalence are the same; this does not mean they are the same logics. We know every first order class of finite models is PTIME and so certainly recursive. But for any set X, the class of linear orders with length in X is definable in L^{3}.

A class is EC_{Δ} if it defined by an infinite conjunction; A class is EC_{Σ} if it defined by an infinite conjunction. A classical result asserts: K is EC_{ΔΣ} iff it is closed under elementary equivalence.

For k-variable logic we have a much stronger condition.

Corollary 0.14 (Kolaitis-Vardi 1992). . Let K be a class of finite models. If K is closed under L^{k} = F O^{k} equivalence then K is definable in L^{k}.

Proof. K is defined by ⋁_{B∈K} ⋀{ϕ ∈ F O^{k} : B ⊧ ϕ}.